perm filename BIRD.LSP[S84,JMC] blob
sn#756741 filedate 1984-05-26 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00004 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 bird.lsp[w84,jmc] Bird circumscription in ekl
C00006 00003 1. (DEFINE A
C00012 00004 (get-proofs bird prf s84 jmc)
C00027 ENDMK
C⊗;
;;; bird.lsp[w84,jmc] Bird circumscription in ekl
(proof bird)
1. (define a |∀ab flies.a(ab,flies) ≡
(∀x.¬ab aspect1 x ⊃ ¬flies x)
∧ (∀x.bird x ⊃ ab aspect1 x)
∧ (∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x)
∧ (∀x.ostrich x ⊃ ab aspect2 x)
∧ (∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x)
|)
2. (axiom |
(∀x y.¬(aspect1 x = aspect2 y))
∧ (∀x y.¬(aspect1 x = aspect3 y))
∧ (∀x y.¬(aspect2 x = aspect3 y))
∧ (∀x y.aspect1 x = aspect1 y ≡ x =y)
∧ (∀x y.aspect2 x = aspect2 y ≡ x =y)
∧ (∀x y.aspect3 x = aspect3 y ≡ x =y)
|)
(label simpinfo)
3. (define a1 |∀ab flies.a1(ab,flies) ≡ a(ab,flies) ∧
∀ab1 flies1.(a(ab1,flies1) ∧ (∀z.ab1 z ⊃ ab z)
⊃ (∀z.ab z ≡ ab1 z))|)
4. (assume |a1(ab,flies)|)
5. (define flies2 |∀x.flies2 x ≡ bird x ∧ ¬ostrich x|)
6. (define ab2 |∀z.ab2 z ≡ (∃x.bird x ∧ z = aspect1 x)
∨ (∃x.ostrich x ∧ z = aspect2 x)|)
7. (rw 4 (open a1))
8. (trw bird#7#1 7)
9. (trw bird#7#2 7)
10. (rw 8 (open a))
11. (assume |ab2 z|)
12. (rw * (open ab2))
13. (derive |ab z| (12 10))
14. (ci (11) 13)
15. (der |∀z.ab2 z ⊃ ab z| 14)
16. (derive |(∀x.¬ab2 aspect1 x ⊃ ¬flies2 x) ∧ (∀x.bird x ⊃ ab2 aspect1 x)
∧ (∀x.bird x ∧ ¬ab2 aspect2 x ⊃ flies2 x) ∧ (∀x.ostrich X ⊃ ab2 aspect2 x)
∧ (∀x.ostrich x ∧ ¬ab2 aspect3 x ⊃ ¬flies2 x)| () (open ab2 flies2))
17. (ue ((ab.ab2) (flies.flies2)) 1)
18. (rw 17 (use 16))
19. (der |∀z.ab z ≡ AB2 Z| (9 15 18))
20. (rw 8 (use 1 mode: exact) ((use 19 mode: exact) (open ab2)))
21. (der |∀x.flies x ≡ bird x ∧ ¬ostrich x| 20)
(save-proofs bird prf s84 jmc)
1. (DEFINE A
|∀AB FLIES.A(AB,FLIES)≡
(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧
(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| NIL)
;labels: SIMPINFO
2. (AXIOM
|(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧
(∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧
(∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)
3. (DEFINE A1
|∀AB FLIES.A1(AB,FLIES)≡
A(AB,FLIES)∧
(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃
(∀Z.AB(Z)≡AB1(Z)))| NIL)
4. (ASSUME |A1(AB,FLIES)|)
;deps: (4)
5. (DEFINE FLIES2 |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| NIL)
6. (DEFINE AB2
|∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))|
NIL)
7. (RW 4 (OPEN A1))
;A(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))
;deps: (4)
8. (TRW |A(AB,FLIES)| (USE 7))
;A(AB,FLIES)
;deps: (4)
9. (TRW |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))|
(USE 7))
;∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))
;deps: (4)
10. (RW 8 (OPEN A))
;(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
;deps: (4)
11. (ASSUME |AB2(Z)|)
;deps: (11)
12. (RW 11 (OPEN AB2))
;(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))
;deps: (11)
13. (DERIVE |AB(Z)| (12 10) NIL)
;AB(Z)
;deps: (4 11)
14. (CI (11) 13 NIL)
;AB2(Z)⊃AB(Z)
;deps: (4)
15. (DERIVE |∀Z.AB2(Z)⊃AB(Z)| (14) NIL)
;∀Z.AB2(Z)⊃AB(Z)
;deps: (4)
16. (DERIVE
|(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧
(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| () (OPEN AB2 FLIES2))
;(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
17. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
;A(AB2,FLIES2)≡
;(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
18. (RW 17 (USE 16))
;A(AB2,FLIES2)
19. (DERIVE |∀Z.AB(Z)≡AB2(Z)| (9 15 18) NIL)
;∀Z.AB(Z)≡AB2(Z)
;deps: (4)
22.
(get-proofs bird prf s84 jmc)
(ttyekl)
(show)
1. (DEFINE A
|ALL AB FLIES.A(AB,FLIES) IFF
(ALL X.NOT AB(ASPECT1(X)) IMP NOT FLIES(X))&
(ALL X.BIRD(X) IMP AB(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB(ASPECT2(X)) IMP FLIES(X))&
(ALL X.OSTRICH(X) IMP AB(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB(ASPECT3(X)) IMP NOT FLIES(X))|
NIL)
;labels: SIMPINFO
2. (AXIOM
|(ALL X Y.NOT ASPECT1(X)=ASPECT2(Y))&(ALL X Y.NOT ASPECT1(X)=ASPECT3(Y))&
(ALL X Y.NOT ASPECT2(X)=ASPECT3(Y))&
(ALL X Y.ASPECT1(X)=ASPECT1(Y) IFF X=Y)&
(ALL X Y.ASPECT2(X)=ASPECT2(Y) IFF X=Y)&
(ALL X Y.ASPECT3(X)=ASPECT3(Y) IFF X=Y)|)
3. (DEFINE A1
|ALL AB FLIES.A1(AB,FLIES) IFF
A(AB,FLIES)&
(ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z))
IMP
(ALL Z.AB(Z) IFF AB1(Z)))| NIL)
4. (ASSUME |A1(AB,FLIES)|)
deps: (4)
5. (DEFINE FLIES2 |ALL X.FLIES2(X) IFF BIRD(X)&NOT OSTRICH(X)| NIL)
6. (DEFINE AB2
|ALL Z.AB2(Z) IFF
(EX X.BIRD(X)&Z=ASPECT1(X)) OR (EX X.OSTRICH(X)&Z=ASPECT2(X))|
NIL)
7. (RW 4 (USE 3 MODE: EXACT))
A(AB,FLIES)&
(ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) IMP
(ALL Z.AB(Z) IFF AB1(Z)))
deps: (4)
8. (TRW |A(AB,FLIES)| (USE 7))
A(AB,FLIES)
deps: (4)
9. (TRW
|ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) IMP
(ALL Z.AB(Z) IFF AB1(Z))| (USE 7))
ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) IMP
(ALL Z.AB(Z) IFF AB1(Z))
deps: (4)
10. (RW 8 (USE 1 MODE: EXACT))
(ALL X.NOT AB(ASPECT1(X)) IMP NOT FLIES(X))&(ALL X.BIRD(X) IMP AB(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB(ASPECT2(X)) IMP FLIES(X))&
(ALL X.OSTRICH(X) IMP AB(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB(ASPECT3(X)) IMP NOT FLIES(X))
deps: (4)
11. (ASSUME |AB2(Z)|)
deps: (11)
12. (RW 11 (OPEN AB2))
(EX X.BIRD(X)&Z=ASPECT1(X)) OR (EX X.OSTRICH(X)&Z=ASPECT2(X))
deps: (11)
13. (DERIVE |AB(Z)| (12 10) NIL)
AB(Z)
deps: (4 11)
14. (CI (11) 13 NIL)
AB2(Z) IMP AB(Z)
deps: (4)
15. (DERIVE |ALL Z.AB2(Z) IMP AB(Z)| (14) NIL)
ALL Z.AB2(Z) IMP AB(Z)
deps: (4)
16. (DERIVE |ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X)| (5 6) NIL)
ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X)
17. (DERIVE |ALL X.BIRD(X) IMP AB2(ASPECT1(X))| (5 6) NIL)
ALL X.BIRD(X) IMP AB2(ASPECT1(X))
18. (DERIVE |ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X)| (5 6) NIL)
ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X)
19. (DERIVE |ALL X.OSTRICH(X) IMP AB2(ASPECT2(X))| (5 6) NIL)
ALL X.OSTRICH(X) IMP AB2(ASPECT2(X))
20. (DERIVE |ALL X.OSTRICH(X) IMP NOT FLIES2(X)| (5 6) NIL)
ALL X.OSTRICH(X) IMP NOT FLIES2(X)
21. (DERIVE |ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X)| (20)
NIL)
ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X)
22. (DERIVE
|(ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X))&
(ALL X.BIRD(X) IMP AB2(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X))&
(ALL X.OSTRICH(X) IMP AB2(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X))|
(16 17 18 19 20 21) NIL)
(ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X))&
(ALL X.BIRD(X) IMP AB2(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X))&
(ALL X.OSTRICH(X) IMP AB2(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X))
23. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
A(AB2,FLIES2) IFF
(ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X))&
(ALL X.BIRD(X) IMP AB2(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X))&
(ALL X.OSTRICH(X) IMP AB2(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X))
24. (RW 23 (USE 22))
A(AB2,FLIES2)
25. (DERIVE |ALL Z.AB(Z) IFF AB2(Z)| (9 15 24) NIL)
ALL Z.AB(Z) IFF AB2(Z)
deps: (4)
26. (RW 8 ((USE 1 MODE: EXACT) ((USE 25 MODE: EXACT) (OPEN AB2))))
(ALL X.NOT (EX X1.BIRD(X1)&X=X1) IMP NOT FLIES(X))&
(ALL X.BIRD(X)&NOT (EX X2.OSTRICH(X2)&X=X2) IMP FLIES(X))&
(ALL X.OSTRICH(X) IMP NOT FLIES(X))
deps: (4)
27. (DERIVE |ALL X.FLIES(X) IFF BIRD(X)&NOT OSTRICH(X)| (26) NIL)
ALL X.FLIES(X) IFF BIRD(X)&NOT OSTRICH(X)
deps: (4)
28.